|
|
A Jabber/XMPP Transport for News via the NNTP Protocol
Halfar, Patrik ; Weiss, Petr (referee) ; Rychlý, Marek (advisor)
This document mention some possibilities of information sharing over computer networks. At the beginning there is described exchange information between group of users by NetNews . Next chapter make short introduction to project Jabber/XMPP and its possibilities. Other part appropriate to possibility combination these services and comment implemented application. There are include descriptions how configure most known Jabber servers for use of this application. There are contain XML schemes of uses files too.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
|
Network Protocols Semiautomatic Diagnostics
Svoboda, Ondřej ; Ryšavý, Ondřej (referee) ; Holkovič, Martin (advisor)
This thesis is about semiautomatic network protocol diagnostics and creating protocol description from eavesdropped communication. Several network eavesdropping techniques and some common programs for network analysis are introduced. Well-known network protocols are described, with focus on their communication messages. Some already existing methods for creating models from examples are mentioned and their characteristics defined. Next we design architecture of developed tool and some methods, that create protocol description. After that we explain implementation of this tool and finally the tool is tested and experimented with.
|
|
| |
|
|
Context-Dependent Scanner
Hatina, Peter ; Koutný, Jiří (referee) ; Čermák, Martin (advisor)
This paper is devoted to principles of a lexical analysis and to a means of context resolution of a lexeme type, depending on its source code position. The lexical analysis, process of a lexical analyzer creation and possible solution for context lexeme recognition, based on a multiple automata system, is described. Lexical analyzer functionality is extended to accept tokens in other languages code blocks.
|
|
|
Implementation of General Disassembler
Přikryl, Zdeněk ; Masařík, Karel (referee) ; Lukáš, Roman (advisor)
This thesis presents the process of creating disassembler for new designed processors. We demand automatic generation of the disassembler. Instruction set for processor is modeled by specialized language ISAC, which offers resources for description of the instruction set. For example it describes format of instruction in the assembly language or format of instruction in the binary form or behavior of this instruction. Internal model is coupled finite automata, which describes relation of textual form of the instruction and binary form of the instruction in formal way. The code of disassembler is generated from the internal model. This disassembler accepts program in binary code at the input and generate equivalent program in assembly language at the output.
|
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Cílem této práce je vývoj technik umožňujících praktické využití nedeterministických konečných automatů, zejména nedeterministických stromových automatů. Jde zvláště o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konečných automatů. V oblasti redukce velikosti vycházíme z dobře známých metod pro slovní automaty které jsou založeny na relacích simulace. Navrhli jsme efektivní algoritmy pro výpočet stromových variant simulačních relací a identifikovali jsme nový typ relace založený na kombinaci takzvaných horních a dolních simulací nad stromovými automaty. Tyto kombinované relace jsou zvláště vhodné pro redukci velikosti automatů slučováním stavů. Navržený princip kombinace relací simulace je relevantní i pro slovní automaty. Náš přínos v oblasti testování jazykové inkluze je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiřetězcové algoritmy, které byly původně navrženy pro slovními automaty. Dále se nám podařilo použitím simulačních relací výrazně zefektivnit protiřetězcové algoritmy pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci našich technik pro praxi jsme demonstrovali jejich nasazením v rámci regulárního stromového model checkingu, což je verifikační metoda založená na stromových automatech. Použití našich algoritmů zde vedlo k výraznému zrychlení a zvětšení škálovatelnosti celé metody. Základní myšlenky našich algoritmů pro redukci velikosti automatů a testování jazykové inkluze jsou aplikovatelné i na jiné typy automatů. Příkladem jsou naše redukční techniky pro alternující Büchiho automaty prezentované v poslední části práce.
|
|
|
Syntactic Analysis Based on Coupled Finite Automata
Zámečníková, Eva ; Masařík, Karel (referee) ; Lukáš, Roman (advisor)
Master's thesis is dealing with translation based on coupled finite automaton model. Coupled finite automaton contains input and output automaton. The input automaton makes syntactic analysis with an input string. Used rules from the input automaton control the output automaton, which generates an output string. In thesis is described a way of determinisation of the input automaton without loss of information about rules used in original automaton. The determinizitaion is divided into two parts - for finite and infinite translation specified by transducers. Then is presented a new pair automaton with increased computing power. This increased computing power consists in replace of input or output or just a part of automaton by context free grammar.
|
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (referee) ; Lengál, Ondřej (advisor)
Presburgerova aritmetika (PrA) je rozhodnutelná teorie přirozených čísel prvního řádu, která nachází uplatnění v mnoha oblastech formální verifikace vlastností softwaru. Řešiče SMT nástroje implementující různé algoritmické přístupy k rozhodování, zda má formule řešení hrají ve formální verifikaci klíčovou roli. V této práci dokumentujeme vytvoření nového automatického SMT řešiče pro PrA založeného na konečných automatech přístupu, který v současnosti žádný SMT řešič nepoužívá. Uvádíme přehled výzev a jejich řešení vyplývajících ze složitosti takového nástroje, včetně výsledků z provedených experimentů, které již identifikují problémy, kde tento alternativní přístup překonává nejmodernější řešiče. Uvádíme také identifikované problémy, u nichž výkonnost postupu založeného na automatech naráží na problémy, které představují otevřené možnosti výzkumu.
|
|
|
Hardware Acceleration of Cipher Attack
Okuliar, Adam ; Slaný, Karel (referee) ; Vašíček, Zdeněk (advisor)
Hardware acceleration is often good tool to achieve significantly better performance of processing great ammount of data or of realization of parallel algoritms. Aim of this work is to demonstrate resoluts of using FPGA circuits for implementation exponentially complex algorithm. As example haschosen brute-force attack on WEP cryptographic algorithm with 40-bit long key. Goal of this work is to compare properties and performance of software and hardware implementation of choosen algorithm.
|
guest ::
